theory ClangSem imports Main Clang
begin

--"local state of a process; 'n - (names of) local variables"
type_synonym 'n pstate = "'n ~=> vals"

datatype 'm ioact =  --"Input-output action by a process; 'm - shared variables"
    ANone            --"No input-output actions"
  | ARead 'm vals    --"ARead x a: read a from shared variable x"
  | AWrite 'm vals   --"AWrite x a: write a to shared variable x"

fun io_read :: "'m ioact \<Rightarrow> bool"
where
  "io_read (ARead _ _) = True"
| "io_read _ = False"

fun io_write :: "'m ioact \<Rightarrow> bool"
where
  "io_write (AWrite _ _) = True"
| "io_write _ = False"

fun var_io :: "'m ioact ~=> 'm"
where
  "var_io ANone = None"
| "var_io (ARead x _) = Some x"
| "var_io (AWrite x _) = Some x"

fun val_io :: "'m ioact ~=> vals"
where
  "val_io ANone = None"
| "val_io (ARead _ a) = Some a"
| "val_io (AWrite _ a) = Some a"

--"process execution step (stmt, state, io action, next stmt, next state)"
datatype ('pn,'n,'m,'l) pstep =
  Pstep "('pn,'n,'m,'l) stmt" "'n pstate" "'m ioact" "('pn,'n,'m,'l) stmt" "'n pstate"

fun pstep_curstm where "pstep_curstm (Pstep s q io s' q') = s"
fun pstep_nxtstm where "pstep_nxtstm (Pstep s q io s' q') = s'"
fun pstep_cur where "pstep_cur (Pstep s q io s' q') = q"
fun pstep_nxt where "pstep_nxt (Pstep s q io s' q') = q'"
fun pstep_io  where "pstep_io  (Pstep s q io s' q') = io"

fun assig :: "'n pstate \<Rightarrow> 'n \<Rightarrow> vals \<Rightarrow> 'n pstate" --"assignment"
where
 "assig q x d = q ++ [x \<mapsto> d]"  --"Note: ++ denotes overlapping"

fun eval_expr :: "'n pstate \<Rightarrow> 'n expr ~=> vals"
where
  "eval_expr q (Evar x) = q x"
| "eval_expr q (Eimm i) = Some i"

fun eval_bexpr :: "'n pstate \<Rightarrow> 'n bexpr ~=> vals"
where
  "eval_bexpr q (Bex e) = eval_expr q e"
| "eval_bexpr q (Beq e1 e2)  =
                    (case (eval_expr q e1) of 
                       (Some _) \<Rightarrow> Some (BoolV (eval_expr q e1 = eval_expr q e2))
                            | _ \<Rightarrow> None)"
| "eval_bexpr q (Bneq e1 e2) =
                    (case (eval_expr q e1) of 
                       (Some _) \<Rightarrow> Some (BoolV (eval_expr q e1 \<noteq> eval_expr q e2))
                            | _ \<Rightarrow> None)"

--"check a wait condition"
fun check_wc :: "('n,'m) wcond \<Rightarrow> 'n pstate \<Rightarrow> 'm ioact \<Rightarrow> bool"
where
  "check_wc (Weq y e) q (ARead y' k') = (y' = y \<and> 
                             (case (eval_expr q e) of 
                                  Some k \<Rightarrow> k' = k 
                                     | _ \<Rightarrow> False))"

| "check_wc (Wneq y e) q (ARead y' k') = (y' = y \<and> 
                             (case (eval_expr q e) of 
                                  Some k \<Rightarrow> k' \<noteq> k
                                     | _ \<Rightarrow> False))"
| "check_wc _ _ _ = False"

--"check disjunction of wait conditions"
fun check_wcs :: "('n,'m) wconds \<Rightarrow> 'n pstate \<Rightarrow> 'm ioact \<Rightarrow> bool"
where
  "check_wcs wcs q io = (\<exists> wc \<in> set wcs . check_wc wc q io)"

fun whexp :: "('pn,'n,'m,'l) stmt \<Rightarrow> ('pn,'n,'m,'l) stmt \<Rightarrow> bool"
where
  "whexp (Cwhile lb be s) (Cseq lb' s1 s') = (lb' = None \<and> s1 = s \<and> s' = (Cwhile lb be s))"
| "whexp _ _ = False"

--"transition s q io s' q' = True iff "
--"if a process executes a statement s on a state q, io is one of the possible"
--"IO actions, s' is the next statement, q' is one of the possible new states"
fun transition :: 
  "('pn,'n,'m,'l) stmt \<Rightarrow> 'n pstate \<Rightarrow> 'm ioact \<Rightarrow> ('pn,'n,'m,'l) stmt \<Rightarrow> 'n pstate \<Rightarrow> bool"
where
  "transition (Cnone lb) q io s' q' = False" (*(io = ANone \<and> s' = (Cnone lb) \<and> q' = q)*)
(* Cnone _ \<Rightarrow> transition s2 q io s' q' *)
(* We use small steps in Cseq and inherit labels in Cnone *)
| "transition (Cseq lb s1 s2) q io s' q' = 
                                (case s1 of
                                   Cnone _ \<Rightarrow> s' = s2 \<and> io = ANone \<and> q' = q
                                    |    _ \<Rightarrow> (case s' of
                                                (Cseq None s1' s2') \<Rightarrow> 
                                                     s2' = s2
                                                   \<and> transition s1 q io s1' q'
                                               | _ \<Rightarrow> False ) )"

| "transition  (Casg lb x (Eimm k)) q io s' q' = 
                             (io = ANone \<and> (s' = Cnone lb) \<and> q' = (assig q x k))"

| "transition  (Casg lb x (Evar y)) q io s' q' = 
                             (io = ANone \<and> (s' = Cnone lb) \<and> 
                                     (case (q y) of
                                           Some k \<Rightarrow> q' = (assig q x k)
                                         | None \<Rightarrow> False ))"

| "transition  (Cif _ be s1 s2) q io s' q' =
                             (io = ANone \<and> q' = q \<and> 
                                     (case (eval_bexpr q be) of 
                                           Some (BoolV True)  \<Rightarrow> s' = s1
                                         | Some (BoolV False) \<Rightarrow> s' = s2
                                         | _ \<Rightarrow> False ))"

| "transition  (Cwhile lb be s) q io s' q' = 
                       (io = ANone \<and> q' = q \<and> 
                           (case (eval_bexpr q be) of
                                Some (BoolV True)  \<Rightarrow> whexp (Cwhile lb be s) s'
                              | Some (BoolV False) \<Rightarrow> (s' = Cnone lb)
                              | _ \<Rightarrow> False ))"

| "transition  (Cread lb x y) q io s' q' = 
                             (s' = (Cnone lb) \<and> 
                                     (case io of 
                                         (ARead y1 k) \<Rightarrow> y1 = y
                                                      \<and> q' = (assig q x k)
                                                  | _ \<Rightarrow> False ))"

| "transition  (Cwrite lb y e) q io s' q' = 
                             (s' = (Cnone lb) \<and> q' = q \<and> 
                                     (case (eval_expr q e) of 
                                             Some k \<Rightarrow> io = AWrite y k
                                           | None \<Rightarrow> False ))"

| "transition  (Cwait _ wcs s) q io s' q' = (s' = s \<and> q' = q \<and> check_wcs wcs q io)"

lemma transit_seq: "transition (Cseq lb s1 s2) q io s' q' =
                 ( (\<exists> lb . s1 = Cnone lb \<and> s' = s2 \<and> io = ANone \<and> q' = q) 
                \<or> (\<exists> s1' . s' = (Cseq None s1' s2) \<and> transition s1 q io s1' q') )"
apply(cases s', simp_all)
apply(cases s1, simp_all)
apply(case_tac "option", simp_all)
apply(cases s1, simp_all)
apply(cases s1, simp_all)
apply(cases s1, simp_all)
apply(cases s1, simp_all)
apply(cases s1, simp_all)
apply(cases s1, simp_all)
apply(cases s1, simp_all)
apply(cases s1, simp_all)
done

fun valid_pstep :: "('pn,'n,'m,'l) pstep \<Rightarrow> bool"
where
  "valid_pstep (Pstep s q io s' q') = transition s q io s' q'"

(*---------------------------------------- *)

--"process execution state"
--"(local variables content, current statement, IO action, active?)"
datatype ('pn,'n,'m,'l) estate
   = Estate "('pn,'n,'m,'l) stmt" "'n pstate" "'m ioact" bool

fun es_active where "es_active (Estate _ _ _ b) = b"

fun es_stm :: "('pn,'n,'m,'l) estate \<Rightarrow> ('pn,'n,'m,'l) stmt"
  where "es_stm (Estate s _ _ _) = s"

type_synonym ('pn,'n,'m,'l) estates = "'pn ~=> ('pn,'n,'m,'l) estate"

--"global program state (execution states of processes, shared variables state)"
datatype ('pn,'n,'m,'l) gstate
   = Gstate "('pn,'n,'m,'l) estates" "'m ~=> vals"

fun gst_ests :: "('pn,'n,'m,'l) gstate \<Rightarrow> ('pn,'n,'m,'l) estates"
where
  "gst_ests (Gstate pes _) = pes"

fun gst_sh :: "('pn,'n,'m,'l) gstate \<Rightarrow> ('m ~=> vals)"
where
  "gst_sh (Gstate _ sh) = sh"

--"global trace - a sequence of global states"
type_synonym ('pn,'n,'m,'l) gtrace = "nat \<Rightarrow> ('pn,'n,'m,'l) gstate"

fun etrans ::"('pn,'n,'m,'l) estate option \<Rightarrow> ('pn,'n,'m,'l) estate option \<Rightarrow> bool"
where
  "etrans (Some (Estate s1 q1 io1 True)) (Some (Estate s2 q2 io2 _)) = 
                                          valid_pstep (Pstep s1 q1 io1 s2 q2)"

| "etrans (Some (Estate s1 q1 io1 False)) es = 
       (es = Some (Estate s1 q1 io1 True) \<or> es = Some (Estate s1 q1 io1 False))"

| "etrans None es = (es = None)"
| "etrans _ _ = False"

lemma etrans_cont: "etrans eso1 eso2 \<Longrightarrow> eso1 \<noteq> None \<Longrightarrow> eso2 \<noteq> None"
apply(cases eso1, cases eso2, auto)
apply(case_tac a, case_tac "bool", auto)
apply(cases eso2, auto)
done

fun eo_io :: "('pn,'n,'m,'l) estate option \<Rightarrow> 'm ioact"
where
  "eo_io (Some (Estate _ _ io True)) = io"
| "eo_io (Some (Estate _ _ io False)) = ANone"
| "eo_io None = ANone"

fun io_compat :: "'m ioact \<Rightarrow> 'm ioact \<Rightarrow> bool"
where
  "io_compat  ANone _ = True"
| "io_compat (ARead x _) (ARead y _) = (x \<noteq> y)"
| "io_compat (ARead x _) (AWrite y _) = (x \<noteq> y)"
| "io_compat (ARead x _) ANone = True"
| "io_compat (AWrite x _) (ARead y _) = (x \<noteq> y)"
| "io_compat (AWrite x _) (AWrite y _) = (x \<noteq> y)"
| "io_compat (AWrite x _) ANone = True"

fun compat_ios:: "('pn,'n,'m,'l) estates \<Rightarrow> bool"
where
  "compat_ios pes = (\<forall> p1 p2 . p1 \<noteq> p2 \<longrightarrow> io_compat (eo_io (pes p1)) (eo_io (pes p2)) )"

fun all_ios:: "('pn,'n,'m,'l) estates \<Rightarrow> 'm ioact set"
where
  "all_ios pes = { io . \<exists> p . io = eo_io (pes p) }"

fun chk_reads :: "'m ioact set \<Rightarrow> ('m ~=> vals) \<Rightarrow> bool"
where
  "chk_reads Io d = (\<forall> x k . (ARead x k) \<in> Io \<longrightarrow> (d x) = (Some k) ) "

fun chk_writes :: "'m ioact set \<Rightarrow> ('m ~=> vals) \<Rightarrow> ('m ~=> vals) \<Rightarrow> bool"
where
  "chk_writes Io d1 d2 = 
           (\<forall> x . (\<not>(\<exists> k . AWrite x k \<in> Io) \<and> d2 x = d1 x) \<or> 
                      (\<exists> k . AWrite x k \<in> Io \<and> d2 x = Some k) ) "

--"global transition:"
--"1) each process either makes a step or waits"
--"2) IO operations by different processes are performed on"
--"   different shared variables"
definition globtrans :: "('pn,'n,'m,'l) estates \<Rightarrow> ('m ~=> vals) \<Rightarrow> 
                                      ('pn,'n,'m,'l) estates \<Rightarrow> ('m ~=> vals) \<Rightarrow> bool"
where
  "globtrans pes1 shm1 pes2 shm2 = 
        ( (\<forall> p . etrans (pes1 p) (pes2 p))
         \<and>  compat_ios pes1
         \<and>  chk_reads (all_ios pes1) shm1
         \<and> chk_writes (all_ios pes1) shm1 shm2 )"

--"is a valid global transition"
fun valid_gtrans :: "('pn,'n,'m,'l) gstate \<Rightarrow> ('pn,'n,'m,'l) gstate \<Rightarrow> bool"
where
  "valid_gtrans (Gstate pes1 shm1) (Gstate pes2 shm2) = 
                                                  globtrans pes1 shm1 pes2 shm2"

--"is a valid global trace"
definition valid_gtrace :: "('pn,'n,'m,'l) gtrace \<Rightarrow> bool"
where
  "valid_gtrace tr = ( \<forall> n . valid_gtrans (tr n) (tr (Suc n)) )"

--"initial state of a given process; note: empty initial local memory"
fun is_proc_inito :: "('pn,'n,'m,'l) proc \<Rightarrow> ('pn,'n,'m,'l) estate option \<Rightarrow> bool"
where
  "is_proc_inito (Proc hdr s) (Some (Estate s0 q0 _ _)) = (s = s0 \<and> q0 = empty)"
| "is_proc_inito _ None = False"

--"initial state of a given program; note: empty initial shared memory"
fun is_prog_init :: "('pn,'n,'m,'l) prog \<Rightarrow> ('pn,'n,'m,'l) gstate \<Rightarrow> bool"
where
  "is_prog_init prog (Gstate pes shm) = 
                 (  shm = empty 
                 \<and> (\<forall> p \<in> set prog . is_proc_inito p (pes (proc_name p)))
                 \<and>  dom pes \<subseteq> set (map proc_name prog) )"

--"semantics of a program is a predicate on global traces"
definition prog_semantics :: "('pn,'n,'m,'l) prog \<Rightarrow> ('pn,'n,'m,'l) gtrace \<Rightarrow> bool"
where
  "prog_semantics prog tr = (is_prog_init prog (tr 0) \<and> valid_gtrace tr)"

end
